Browse by Tags: formal methods

Up a level
Export as [feed] Atom [feed] RSS 1.0 [feed] RSS 2.0
Number of items: 62.
  1. [img] [img]
    COMP1216 - AY2023-24 - Coursework 2
    Event-B Model for a Dentist Appointment System

    Shared with the University by
    Dr Son Hoang
  2. [img] [img]
    COMP1216 - An Exercise in Modelling using Relations
    Shared with the University by
    Dr Son Hoang
  3. [img] [img]
    COMP1216 - Coursework - An Auction System
    Shared with the University by
    Dr Son Hoang
  4. [img]
    COMP1216 - Coursework 2 (2020-21)
    Description of Coursework 2 for COMP1216 (2020-21)

    Shared with the University by
    Dr Son Hoang
  5. [img] [img]
    COMP1216 - Extending Access Control Model with Tokens and Time
    Shared with the University by
    Dr Son Hoang
  6. [img] [img]
    COMP1216 - Extending Event-B Model
    Shared with the University by
    Dr Son Hoang
  7. [img] [img]
    COMP1216 - Lab 05 - Modelling with Sets in Event-B
    Modelling with Sets in Event-B

    Shared with the University by
    Dr Son Hoang
  8. [img] [img]
    COMP1216 - Lab 6 - Modelling with Relations in Event-B
    Modelling using Relations in Event-B

    Shared with the University by
    Dr Son Hoang
  9. [img] [img]
    COMP1216 - Lab 7 - A Hotel Reception System in Event-B
    Model a hotel reception system in Event-B

    Shared with the University by
    Dr Son Hoang
  10. [img] [img]
    COMP1216 - Lab 8 - Multiple Hotel System in Event-B
    Managing room allocation in multiple hotels in Event-B

    Shared with the University by
    Dr Son Hoang
  11. [img] [img]
    COMP1216 - Lab 9 - Port Management System in Event-B
    Port Management system in Event-B

    Shared with the University by
    Dr Son Hoang
  12. [img]
    COMP1216 - Lecture 07 - Introducing Event-B
    Introducing Event-B (Contexts, machines)

    Shared with the University by
    Dr Son Hoang
  13. [img] [img]
    COMP1216 - Modelling Classes and Associations
    Shared with the University by
    Dr Son Hoang
  14. [img]
    COMP1216 - Proof-based Verification in Event-B
    Shared with the University by
    Dr Son Hoang
  15. [img]
    COMP1216 - Relations in Event-B
    Modelling using Relations in Event-B - Order Pairs - Cartesian Product - Relations - Domain/Range of relations - Relational Image

    Shared with the University by
    Dr Son Hoang
  16. [img] [img]
    COMP1216 - Revision
    Revision

    Shared with the University by
    Dr Son Hoang
  17. [img] [img]
    COMP1216 - Solving Puzzles with Invariants
    - "Chameleons of three colours" riddle

    Shared with the University by
    Dr Son Hoang
  18. [img] [img]
    COMP1216 - What Next? ... How about Program Verification?
    Shared with the University by
    Dr Son Hoang
  19. [img] [img]
    COMP1216 Coursework 2 (AY2022-23)
    Coursework 2: Event-B modelling of an auction system

    Shared with the University by
    Dr Son Hoang
  20. collection
    COMP1216 Software Modelling and Design (AY2020-21)
    Shared with the University by
    Dr Son Hoang
  21. [img] [img]
    COMP2214 - Coursework (AY2024-25)
    MULTI elevator coursework

    Shared with the University by
    Dr Son Hoang
  22. [img] [img]
    COMP2214 - Coursework AY2022-23
    Shared with the University by
    Dr Son Hoang
  23. [img] [img]
    COMP2214 - Coursework AY2023-24
    MULTI elevator coursework

    Shared with the University by
    Dr Son Hoang
  24. [img] [img]
    COMP2214 - Coursework descriptions 2020-21
    Shared with the University by
    Dr Son Hoang
  25. [img] [img]
    COMP2214 - Lecture 00 - Introduction
    Introduction to Advanced Software Modelling & Design

    Shared with the University by
    Dr Son Hoang
  26. [img] [img]
    COMP2214 - Lecture 01 - Proof-based verification in Event-B
    Proof-based Verification in Event-B

    Shared with the University by
    Dr Son Hoang
  27. [img] [img]
    COMP2214 - Lecture 02 - Deductive Proof (Propositional Logic)
    - Constructing Proof Trees - Inference Rules - Applying inference rules backwardly to construct proof trees

    Shared with the University by
    Dr Son Hoang
  28. [img] [img]
    COMP2214 - Lecture 03 - Deductive Proof (First-Order Logic and Set Theory)
    Shared with the University by
    Dr Son Hoang
  29. [img] [img]
    COMP2214 - Lecture 04 - Set Theory
    A refresher on Set Theory

    Shared with the University by
    Dr Son Hoang
  30. [img] [img]
    COMP2214 - Lecture 05 - Tree File
    - Tree file system - Transitive Closure

    Shared with the University by
    Dr Son Hoang
  31. [img] [img]
    COMP2214 - Lecture 06 - Reachability in Transition System
    Shared with the University by
    Dr Son Hoang
  32. [img] [img]
    COMP2214 - Lecture 07 - Debugging Models with Proof and Judgement
    Debugging Models with Proof and Judgement - Strengthen Guards - Modify Actions - Strengthen Invariants - Weaken Invariants

    Shared with the University by
    Dr Son Hoang
  33. [img] [img]
    COMP2214 - Lecture 08 - Extension Refinement
    - Abstraction & Refinement - Extension Refinement

    Shared with the University by
    Dr Son Hoang
  34. [img] [img]
    COMP2214 - Lecture 09 - Extension Refinement with Guard Modification
    Shared with the University by
    Dr Son Hoang
  35. [img] [img]
    COMP2214 - Lecture 10 - Data Refinement
    Shared with the University by
    Dr Son Hoang
  36. [img] [img]
    COMP2214 - Lecture 11- Convergence and Deadlock-freeness
    Shared with the University by
    Dr Son Hoang
  37. [img] [img]
    COMP2214 - Lecture 12 - An Elevator System
    Shared with the University by
    Dr Son Hoang
  38. [img]
    COMP2214 - Lecture 13 - Contracts
    Slides from Prof Michael Butler

    Shared with the University by
    Dr Son Hoang
  39. [img]
    COMP2214 - Lecture 14 - Loops
    Reasoning about looping programs

    Shared with the University by
    Dr Son Hoang
  40. [img] [img]
    COMP2214 - Lecture 15 - Introduction to Ada
    Introduction to Ada programming language

    Shared with the University by
    Dr Son Hoang
  41. [img] [img]
    COMP2214 - Lecture 15 - Verification in Dafny
    Verification in Dafny

    Shared with the University by
    Dr Son Hoang
  42. [img] [img]
    COMP2214 - Lecture 16 - Event-B to Dafny
    Shared with the University by
    Dr Son Hoang
  43. [img] [img]
    COMP2214 - Lecture 16 - Introduction to SPARK
    Introductory slides on SPARK

    Shared with the University by
    Dr Son Hoang
  44. [img]
    COMP2214 - Lecture 17 - System Theoretic Process Analysis
    Shared with the University by
    Dr Son Hoang
  45. [img]
    COMP2214 - Lecture 18 - Requirements Engineering
    Shared with the University by
    Dr Son Hoang
  46. [img] [img]
    COMP2214 - Lecture 21 - Revision
    Revision lecture

    Shared with the University by
    Dr Son Hoang
  47. [img] [img]
    COMP2214 - Past Exams
    Past exams paper for COMP2214.

    Shared with the University by
    Dr Son Hoang
  48. [img]
    COMP2214 - Problem Class 00 - Introduction to the Rodin Platform
    Shared with the University by
    Dr Son Hoang
  49. [img] [img]
    COMP2214 - Problem Class 01 - Deductive Proof (Propositional Logic)
    Exercises for Propositional Logic Proof in Rodin Platform

    Shared with the University by
    Dr Son Hoang
  50. [img] [img]
    COMP2214 - Problem Class 02 - Deductive Proof (Predicate Logic and Set Theory)
    Exercises for Predicate Logic and Set Theory Proof in Rodin Platform

    Shared with the University by
    Dr Son Hoang
  51. [img] [img]
    COMP2214 - Problem Class 03 - Model a Routing System
    Model a Routing System using transitive closure

    Shared with the University by
    Dr Son Hoang
  52. [img] [img]
    COMP2214 - Problem Class 04 - Fixing models using failing proofs
    Fixing models using failing proofs

    Shared with the University by
    Dr Son Hoang
  53. [img] [img]
    COMP2214 - Problem Class 05 - Extension Refinement with Guard Modification
    Shared with the University by
    Dr Son Hoang
  54. [img] [img]
    COMP2214 - Problem Class 06 - Hoare Logic
    Exercises on Hoare Logic

    Shared with the University by
    Dr Son Hoang
  55. [img] [img]
    COMP2214 - Problem Class 07 - Hoare Logic in SPARK
    Exercises on Hoare Logic in SPARK - Flow analysis - Pre-/Post-conditions - Loops: Invariants, Variants

    Shared with the University by
    Dr Son Hoang
  56. [img] [img]
    COMP2214 - Problem Class 08 - Elevator System in SPARK
    Exercise using the Elevator System in SPARK

    Shared with the University by
    Dr Son Hoang
  57. [img]
    COMP2214 - Proof rules
    Some useful proof rules

    Shared with the University by
    Dr Son Hoang
  58. [img] [img]
    COMP2214 - Tutorial 6 - Verification with Dafny (part 1)
    Shared with the University by
    Dr Son Hoang
  59. [img] [img]
    COMP2214 - Tutorial 7 - Verification with Dafny (part 2)
    Shared with the University by
    Dr Son Hoang
  60. collection
    COMP2214 Advanced Software Modelling and Design
    Shared with the University by
    Dr Son Hoang
  61. [img] [img]
    COMP2214 Lecture 17 - Event-B to SPARK
    This lecture about data refinement from Event-B models and generating SPARK/Ada from the model

    Shared with the University by
    Dr Son Hoang
  62. [img] [img]
    Modelling Dojo: The SmarTaxi Case Study
    We illustrate the modelling activities using the SmarTaxi Case Study

    Shared with the University by
    Dr Son Hoang
This list was generated on Sat Apr 12 12:25:59 2025 UTC.